/*
Copyright 2017 Bjoern Lellman, Marianna Girlando, Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis. 
This file is part of VINTE. VINTE is free software: you can redistribute it and/or modify it under 
the terms of the GNU General Public License as published by the Free Software Foundation, either version 
3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will 
be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR 
A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy 
of the GNU General Public License along with VINTE. If not, see <http://www.gnu.org/licenses/>.
*/


/* 

To run NESCOND and VINTE on 76 valid formulas (obtained by translating modal K valid formulas from Heuerding-Beckert-Gorè),
run:

comparison(MSec)
checkValid(MSec)

MSec=timeout.

To list K valid formulas, run:
listOfValidFormulas(List).

*/

:- op(400,fy,-), 
   op(500,xfy,&), 
   op(600,xfy,v), 
   op(800,xfy,<=>),
   op(400,fy,box), 
   op(400,fy,dia),
   op(400,fy,neg), 
   op(500,xfy,and), 
   op(600,xfy,or),
   op(700,xfy,->), 
   op(700,xfy,=>),
   op(400,xfy,^),
   op(600,xfy,?),
   op(700,xfy,<).
   
:-use_module(library(random)).
:-use_module(library(lists)).
:-use_module(library(timeout)).
:-use_module(library(ordsets)).



/* This predicate finds all the labels in the sequent 
      etichette(+Sequente,-ListaEtichette) */
etichette([],[]):-!.
etichette([[L,_]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L,_,L]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1,L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),\+member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L2,TailLab),member(L1,TailLab),!.
etichette([_|Tail],Labels):-etichette(Tail,Labels).

/* This predicate creates a partition of the sequent in atomic, transition and complex formulas */
struttura([],[],[],[]):-!.
struttura([[X,A and B]|Tail],Literal,Transaction,[[X,A and B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A or B]|Tail],Literal,Transaction,[[X,A or B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A -> B]|Tail],Literal,Transaction,[[X,A -> B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A => B]|Tail],Literal,Transaction,[[X,A => B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,neg A]|Tail],Literal,Transaction,[[X,neg A]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A,Y]|Tail],Literal,[[X,A,Y]|TransTail],Formulae):-
  struttura(Tail,Literal,TransTail,Formulae),!.
struttura([X|Tail],[X|LitTail],Transition,Formulae):-
  struttura(Tail,LitTail,Transition,Formulae),!.

/* This predicate inserts a formula in the correct list; more precisely, a formula
   can be an atomic formula or a complex formula */
put([X,A and B],Literal,Formulae,Literal,[[X,A and B]|Formulae]):-!.
put([X,A or B],Literal,Formulae,Literal,[[X,A or B]|Formulae]):-!.
put([X,A -> B],Literal,Formulae,Literal,[[X,A -> B]|Formulae]):-!.
put([X,A => B],Literal,Formulae,Literal,[[X,A => B]|Formulae]):-!.
put([X,neg A],Literal,Formulae,Literal,[[X,neg A]|Formulae]):-!.
put(X,Literal,Formulae,[X|Literal],Formulae):-!.




/* Nested sequent calculi */
removeLabels([],[]):-!.
removeLabels([[_,Fml]|Tail],[Fml|ResTail]):-removeLabels(Tail,ResTail).
createConj([Singleton],Singleton):-!.
createConj([Head|Tail],Head and FmlTail):-createConj(Tail,FmlTail).
createNestedSequent(KB,Fml):-removeLabels(KB,KBUnlab),createConj(KBUnlab,Fml).


fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!,
								  append(TempNS,ListToFill,NewNS).
fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals]|TempNS]):-select([[Fml,Gamma],AppliedConditionals],NS,TempNS),
								  fillTheHole(Gamma,ListToFill,NewGamma).

selectList([],NS,[hole|NS]).
selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS),
								 selectList(Tail,TempNS,NewNS).
						
deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS).
deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals]|NewNS]):-select([[Fml,Gamma],AppliedConditionals],NS,NewNS),
						   deepSelect(List,Gamma,NewGamma).

memberList([],_):-!.
memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS).
deepMember(List,NS):-memberList(List,NS),!.
deepMember(List,NS):-member([[_,Gamma],_],NS),
					 deepMember(List,Gamma),!.

/* Axioms closing branches */
proveNS(NS):-deepMember([P,neg P],NS),!.
proveNS(NS):-deepMember([true],NS),!.
proveNS(NS):-deepMember([neg false],NS),!.
/* Rules with one premise */
proveNS(NS):-deepSelect([neg neg A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A or B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([neg (A and B)],NS,NewNS),!,fillTheHole(NewNS,[neg A,neg B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[neg A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[]]],DefNS),proveNS(DefNS).
/* Rules with two or three premises (introducing a branch in a backward proof search) */
proveNS(NS):-deepSelect([neg (A or B)],NS,NewNS),!,fillTheHole(NewNS,[neg A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([A and B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([neg (A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-
    deepSelect([neg (A => B),[[C,Delta],AppliedConditionals]],NS,NewNS),
    \+member(neg (A => B),AppliedConditionals),!,
    proveNS([A,neg C]),
    proveNS([C,neg A]),
    fillTheHole(NewNS,[neg(A => B),[[C,[neg B|Delta]],[neg (A => B)|AppliedConditionals]]],DefNS),
    proveNS(DefNS).




/* Internal calculi for logic VN */

/* Axioms closing branches */
proveVINTE([Gamma,Delta],tree(axb,[Gamma,Delta],no,no)):-member(false,Gamma),!.
proveVINTE([Gamma,Delta],tree(axt,[Gamma,Delta],no,no)):-member(true,Delta),!.
proveVINTE([Gamma,Delta],tree(init,[Gamma,Delta],no,no)):-member(P,Gamma),member(P,Delta),!.


/* Rules with one premise */
proveVINTE([Gamma,Delta],tree(negL,[Gamma,Delta],SubTree,no)):-
  select(-A,Gamma,NewGamma),\+member(A,Delta),!,proveVINTE([NewGamma,[A|Delta]],SubTree).
proveVINTE([Gamma,Delta],tree(negR,[Gamma,Delta],SubTree,no)):-
  select(-A,Delta,NewDelta),\+member(A,Gamma),!,proveVINTE([[A|Gamma],NewDelta],SubTree).
proveVINTE([Gamma,Delta],tree(impR,[Gamma,Delta],SubTree,no)):-
  select(A->B,Delta,NewDelta),(\+member(A,Gamma);\+member(B,NewDelta)),!,proveVINTE([[A|Gamma],[B|NewDelta]],SubTree).
proveVINTE([Gamma,Delta],tree(andL,[Gamma,Delta],SubTree,no)):-
  select(A^B,Gamma,NewGamma),(\+member(A,NewGamma);\+member(B,NewGamma)),!,proveVINTE([[A,B|NewGamma],Delta],SubTree).
proveVINTE([Gamma,Delta],tree(orR,[Gamma,Delta],SubTree,no)):-
  select(A ? B,Delta,NewDelta),(\+member(A,NewDelta);\+member(B,NewDelta)),!,proveVINTE([Gamma,[A,B|NewDelta]],SubTree).
proveVINTE([Gamma,Delta],tree(precR,[Gamma,Delta],SubTree,no)):-
  select(A < B,Delta,NewDelta),\+memberOrdSet([[A],B],Delta),!,proveVINTE([Gamma,[[[A],B]|NewDelta]],SubTree).
proveVINTE([Gamma,Delta],tree(n,[Gamma,Delta],SubTree,no)):-
  \+memberOrdSet([[false],true],Delta),Gamma \== [true],Delta \== [false],!,proveVINTE([Gamma,[[[false],true]|Delta]],SubTree).
proveVINTE([Gamma,Delta],tree(condR,[Gamma,Delta],SubTree,no)):-
  select(A=>B,Delta,NewDelta),
  (\+member((A^(-B)) < A,Gamma);\+memberOrdSet([[false],A],NewDelta)),
  !,
  proveVINTE([[(A^(-B)) < A|Gamma],[[[false],A]|NewDelta]],SubTree).  

/* Rules with two premises */
proveVINTE([Gamma,Delta],tree(impL,[Gamma,Delta],Sub1,Sub2)):-
  select(A->B,Gamma,NewGamma),\+member(B,NewGamma),\+member(A,Delta),!,proveVINTE([[B|NewGamma],Delta],Sub1),proveVINTE([NewGamma,[A|Delta]],Sub2).
proveVINTE([Gamma,Delta],tree(andR,[Gamma,Delta],Sub1,Sub2)):-
  select(A^B,Delta,NewDelta),\+member(A,NewDelta),\+member(B,NewDelta),!,proveVINTE([Gamma,[A|NewDelta]],Sub1),proveVINTE([Gamma,[B|NewDelta]],Sub2).
proveVINTE([Gamma,Delta],tree(orL,[Gamma,Delta],Sub1,Sub2)):-
  select(A ? B,Gamma,NewGamma),\+member(A,NewGamma),\+member(B,NewGamma),!,proveVINTE([[A|NewGamma],Delta],Sub1),proveVINTE([[B|NewGamma],Delta],Sub2).
proveVINTE([Gamma,Delta],tree(condL,[Gamma,Delta],Sub1,Sub2)):-
  select(A => B,Gamma,NewGamma),
  \+member(false < A,NewGamma),\+memberOrdSet([[A ^ (-(B))],A],Delta),!,
  proveVINTE([[false < A|NewGamma],Delta],Sub1),
  proveVINTE([NewGamma,[[[A^(-B)],A]|Delta]],Sub2).
proveVINTE([Gamma,Delta],tree(precL,[Gamma,Delta],Sub1,Sub2)):-
  member(A < B,Gamma),select([Sigma,C],Delta,NewDelta),
  remove_duplicates([B|Sigma],NewSigma),
  \+memberOrdSet([NewSigma,C],Delta),
  \+memberOrdSet([Sigma,A],Delta),!,
  proveVINTE([Gamma,[[NewSigma,C]|NewDelta]],Sub1),
  proveVINTE([Gamma,[[Sigma,A]|Delta]],Sub2).
proveVINTE([Gamma,Delta],tree(com,[Gamma,Delta],Sub1,Sub2)):-
  select([Sigma1,A],Delta,Temp),
  select([Sigma2,B],Temp,NewDelta),
  append(Sigma1,Sigma2,NewSigma),
  remove_duplicates(NewSigma,SigmaDef),
  \+memberOrdSet([SigmaDef,A],Delta),
  \+memberOrdSet([SigmaDef,B],Delta),
  !,
  proveVINTE([Gamma,[[SigmaDef,A],[Sigma2,B]|NewDelta]],Sub1),
  proveVINTE([Gamma,[[SigmaDef,B],[Sigma1,A]|NewDelta]],Sub2).

/* Jump rule */
proveVINTE([Gamma,Delta],tree(jump,[Gamma,Delta],SubTree,no)):-member([Sigma,A],Delta),proveVINTE([[A],Sigma],SubTree).



% memberOrdSet([Sigma,A],Delta)
% It succeeds if and only if Delta contains a block [Psi,A] such that Sigma \subseteq Psi - To this aim, ordsets are used to compare sets corresponding to lists of formulas
memberOrdSet([Sigma,A],Delta):-
list_to_ord_set(Sigma,SigmaOrdSet),
member([Psi,A],Delta),
list_to_ord_set(Psi,PsiOrdSet),
%ord_seteq(SigmaOrdSet,PsiOrdSet).
ord_subset(SigmaOrdSet,PsiOrdSet).



% It removes duplicated items in the list
remove_duplicates([],[]):-!.
remove_duplicates([Head|Tail],NewTail):-member(Head,Tail),!,remove_duplicates(Tail,NewTail).
remove_duplicates([Head|Tail],[Head|NewTail]):-remove_duplicates(Tail,NewTail).


comparison(Ms):-
  write('...loading examples...\n'),
  listOfValidFormulas(ListModLean),
  write('...DONE...\n'),
  write('...converting modal formulas...\n'),
  convertList(ListModLean,ListCond),
  convertListVINTE(ListCond,ListVINTE),
  write('...DONE...\n'),
  retractall(succ(_)),
  retractall(to(_)),
  retractall(fail(_)),
  retractall(succV(_)),
  retractall(toV(_)),
  retractall(failV(_)),
  retractall(listFail(_)),
  asserta(succ(0)),
  asserta(to(0)),
  asserta(fail(0)),
  asserta(succV(0)),
  asserta(toV(0)),
  asserta(failV(0)),
  asserta(listFail(0)),
  write('\n -------------- NESCOND --------------- \n'),
  statList(ListCond,Ms),
  succ(NS),
  to(NTO),
  write('\n -------------- VINTE --------------- \n'),
  statListVINTE(ListVINTE,Ms),
  succV(VS),
  toV(VTO),
  failV(VF),
  listFail(ListOfFail),
%  write('Fallimento su: '),
%  write(ListOfFail),
  write('\n\n'),
  write('Succ    TO    No \n'),
  write(NS),write('       '),
  write(NTO),write('       '),
  write(VF),write('\n'),
  write(VS),write('       '),
  write(VTO),write('       '),
  write(VF),write('\n').

checkValid(Ms):-
  listOfValidFormulas(ListModLean),
  convertList(ListModLean,ListCond),
  convertListVINTE(ListCond,ListVINTE),
  retractall(succ(_)),
  retractall(to(_)),
  retractall(fail(_)),
  retractall(succV(_)),
  retractall(toV(_)),
  retractall(failV(_)),
  retractall(listFail(_)),
  asserta(succ(0)),
  asserta(to(0)),
  asserta(fail(0)),
  asserta(succV(0)),
  asserta(toV(0)),
  asserta(failV(0)),
  asserta(listFail(0)),
  statList(ListCond,Ms),
  succ(NS),
  to(NTO),
  write('\n\n'),
  statListVINTE(ListVINTE,Ms),
  write('\n\n'),
  succV(VS),
  toV(VTO),
  failV(VF).



statList([],_):-!.
statList([[Label,Fml]|Tail],Ms):-(
  time_out(
    (
      proveNS([neg (Fml)])
    ),Ms,Result),!,
  (
    (
    Result=success,!,
    succ(N),retractall(succ(_)),N1 is N+1,asserta(succ(N1)),
    write('o'),
    statList(Tail,Ms)
    );
    (
    to(T),retractall(to(_)),T1 is T+1,asserta(to(T1)),
    write('-'),
    statList(Tail,Ms)
    )
  )
  )
;
(
  fail(NF),
  listFail(LF),
  retractall(fail(_)),
  retractall(listFail(_)),
  N1 is NF+1,
  asserta(fail(N1)),
  asserta(listFail([Label|LF])),
  write('failNESCOND--'),
  statList(Tail,Ms)
	).

statListVINTE([],_):-!.
statListVINTE([Fml|Tail],Ms):-(
  time_out(
    (
      proveVINTE([[Fml],[]],_)
    ),Ms,Result),!,
  (
    (
    Result=success,!,
    succV(N),retractall(succV(_)),N1 is N+1,asserta(succV(N1)),
    write('o'),
    statListVINTE(Tail,Ms)
    );
    (
    write('-'),
    toV(T),retractall(toV(_)),T1 is T+1,asserta(toV(T1)),
    statListVINTE(Tail,Ms)
    )
  )
  )
;
(
  fail(VF),
  listFail(LF),
  retractall(failV(_)),
  retractall(listFail(_)),
  V1 is VF+1,
  asserta(failV(V1)),
  asserta(listFail([LF])),
  statListVINTE(Tail,Ms),
  write('FailVINTE--')
  ).

convertList([],[]):-!.
convertList([[Label,_,Fml]|Tail],[[Label,ConvFml]|ResTail]):-convertFml(Fml,ConvFml),convertList(Tail,ResTail).
convertFml(-A,neg (CA)):-!,convertFml(A,CA).
convertFml(A & B,CA and CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(A v B,CA or CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(A -> B,CA -> CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(box A,true => CA):-!,convertFml(A,CA).
convertFml(dia A,neg (true => neg (CA))):-!,convertFml(A,CA).
convertFml(P,P):-!.

convertListVINTE([],[]):-!.
convertListVINTE([[_,Fml]|Tail],[FMlVINTE|VINTETail]):-convertFmlVINTE(Fml,FMlVINTE),convertListVINTE(Tail,VINTETail).
convertFmlVINTE(neg A,-(CA)):-!,convertFmlVINTE(A,CA).
convertFmlVINTE(A and B,CA ^ CB):-!,convertFmlVINTE(A,CA),convertFmlVINTE(B,CB).
convertFmlVINTE(A or B,CA ? CB):-!,convertFmlVINTE(A,CA),convertFmlVINTE(B,CB).
convertFmlVINTE(A -> B,CA -> CB):-!,convertFmlVINTE(A,CA),convertFmlVINTE(B,CB).
convertFmlVINTE(A => B,(CA) => (CB)):-!,convertFmlVINTE(A,CA),convertFmlVINTE(B,CB).
convertFmlVINTE(P,P):-!.

listOfValidFormulas([
    [t1,2,-((box(p -> q)) -> ((box p) -> (box q)))],
    [t2,2,-(((box(p & q))) -> ((box p) & (box q)))],
	[t3,2,-(((box p) & (box (p -> q))) -> (box q))],
    [t4,2,-((((box p) & (dia (-q))) -> (dia (p & (-q)))))],
    [t5,2,-((((dia p) v (dia q)) -> (dia(p v q))))],
    [t6,2,(-(((box(p -> q)) -> ((box p) -> (box q))) &
	           (((box(p & q))) -> ((box p) & (box q))) & 
	           (((box p) & (box (p -> q))) -> (box q)) &
	           ((((box p) & (dia (-q))) -> (dia (p & (-q))))) &
	           ((((dia p) v (dia q)) -> (dia(p v q))))))],
    [raj6e1a1, 3, ((box (q v -(p))) & (box (p) & box (box q) & box (box
	                    q)) & dia -(p) & dia -(q))],  
    [raj6e1a2, 3, ((box (q v -(p))) & (box (p) & box (box q) & box (p))
	                    & dia -(p) & dia -(q))],
    [raj6e1b, 3, ((box (q v -(p))) & (box (p) & box (box p) & box (p v
	                    box q)) & dia -(p) & dia -(q))],
     [lwb4, 40, -(box p1 v box p2 v box p3 v box p5 v (dia (-p1 & box
	                p3) v dia (-p1 & box p5) v dia (-p2 & box p1) v (dia
	                (-p3 & box p3) v dia (-p3 & box p5)) v (dia (-p5 & box
	                p3) v dia (-p5 & box p5)) v (dia dia (-p1 & box p1) v
	                dia dia (-p1 & box p3) v dia dia (-p1 & box p4) v dia
	                dia (-p1 & box p5)) v (dia (-p4 & box p2) v dia (-p6 &
	                box p2)) v (dia dia (-p3 & box p1) v dia dia (-p3 &
	                box p3) v dia dia (-p3 & box p5)) v (dia (-p4 & box
	                p4) v dia (-p6 & box p4)) v (dia dia (-p5 & box p1) v
	                dia dia (-p5 & box p3) v dia dia (-p5 & box p5)) v
	                (dia (-p4 & box p6) v dia (-p6 & box p6)) v (dia dia
	                dia (-p1 & box p3) v dia dia dia (-p1 & box p5)) v
	                (dia dia (-p2 & box p2) v dia dia (-p4 & box p2) v dia
	                dia (-p6 & box p2)) v (dia dia dia (-p3 & box p3) v
	                dia dia dia (-p3 & box p5)) v (dia dia dia (-p4 & box
	                p1) v (dia dia (-p2 & box p4) v dia dia (-p4 & box p4)
	                v dia dia (-p6 & box p4))) v (dia dia dia (-p5 & box
	                p3) v dia dia dia (-p5 & box p5)) v (dia dia (-p2 &
	                box p6) v dia dia (-p4 & box p6) v dia dia (-p6 & box
	                p6)) v (dia dia dia (-p2 & box p2) v dia dia dia (-p6
	                & box p2)) v (dia dia dia (-p2 & box p4) v dia dia dia
	                (-p6 & box p4)) v (dia dia dia (-p2 & box p6) v dia
	                dia dia (-p6 & box p6))) v (dia dia dia dia -p2 v dia
	                dia dia dia -p4 v dia dia dia dia -p1 v dia dia dia
	                dia -p6))],
    [tx1,10,-((box p -> dia p) -> dia true)],
    [tx2,10,-((dia true -> box p -> dia p))],
    [tx3,10,-((box p -> box box p) -> box p & dia q -> dia (box p & q))],
    [tx4,10,-((box p & dia -box p -> dia (box p & -box p)) -> box p ->
	              box box p)],
    [tx5,10,-((dia p -> box dia p) -> dia p & dia q -> dia (dia p & q))],
    [tx6,10,-((dia p & dia -dia p -> dia (dia p & -dia p)) -> dia p ->
	              box dia p)],
    [tx7,10,-((p -> box dia p) -> p & dia q -> dia (dia p & q))],
    [tx8,10,-((p & dia -dia p -> dia (dia p & -dia p)) -> p -> box dia p)],
    [tx9,10,-((box false -> false) -> box p -> dia p)],
    [tx10,10,-((box dia -p -> dia -p) & (dia box p -> box dia box p) &
	               box (dia -p -> box dia -p) -> box p -> box box p)],
    [tx11,10,-((box -p -> -p) & (dia p -> box dia p) -> p -> box dia p)],
    [tx12,10,-((box (box -p -> box box -p) & (dia p -> box dia dia p)
	               -> dia p -> box dia p))],
    [tx13,10,-((box (dia -p -> box dia -p) & (box p -> box dia box p)
	               -> box p -> box box p))],
    [tx14,10,-((box p -> dia p) & (box p -> box box p) & (-p -> box dia
	               -p) -> box p -> p)],
    [tx15,10,-((dia box q -> box dia q) -> dia (p & box q) -> box (p v
	               dia q))],
    [tx16,10,-((box (box p -> dia p) & (dia (box p & box p) -> box (box
	               p v dia p)) -> dia box p -> box dia p))],
    [tx17,3,-((box (p & box p -> q) v box (q & box q -> p) -> box (p v
	               q) & box (box p v q) & box (p v box q) -> box p v box q))],
    [tx18,10,-((box ((p & box p -> q) v (q & box q -> p)) & box (box (p
	               & box p -> q) v (q & box q -> p)) & box ((p & box p ->
	               q) v box (q & box q -> p)) -> box (p & box p -> q) v
	               box (q & box q -> p)) -> box (p & box p -> q) v box (q
	               & box q -> p))],
    [tx19,10,-((box (box p -> q) v box (box q -> p) -> box (box p v q)
	               & box (p v box q) -> box p v box q))],
    [tx20,10,-((box (box (box p -> q) v (box q -> p)) & box ((box p ->
	               q) v box (box q -> p)) -> box (box p -> q) v box (box q
	               -> p)) -> box (box p -> q) v box (box q -> p))],
    [tx21,10,-((box (box p -> q) v box (box q -> p) -> box (p & box p
	               -> q) v box (q & box q -> p)))],
    [tx22,10,-((box (box p -> p) & box (box q -> q) & (box (p & box p
	               -> q) v box (q & box q -> p)) -> box (box p -> q) v box
	               (box q -> p)))],
    [tx23,10,-((box (box p -> p) & box (box q -> q) & (box (box p ->
	               box q) v box (box q -> box p)) -> box (box p -> q) v
	               box (box q -> p)))],
    [tx24,10,-((box (p & box p -> q) -> box box (p & box p -> q)) &
	               (box (q & box q -> p) -> box box (q & box q -> p)) &
	               box (box p -> box box p) & box (box q -> box box q) &
	               (box (p & box p -> q) v box (q & box q -> p)) -> box
	               (box p -> box q) v box (box q -> box p))],
    [tx25,10,-((dia box p -> box dia box p) & box (dia -p -> box dia
	               -p) -> box (box p -> box q) v box (box q -> box p))],
    [tx26,10,-((box (box -p -> dia -p) & (box (box p -> box -p) v box
	               (box -p -> box p)) -> dia box p -> box dia p))],
    [tx27,5,-((dia p -> box dia p) & (dia -p -> box dia -p) -> dia box
	               p -> box dia p)],
    [tx28,10,-((box (box dia p -> dia box p) -> box dia p -> dia box p)
	               & box (box p -> box box p) & box (box dia p -> dia box
	               p) -> dia box (p -> box p))],
    [tx29,10,-((box dia box (p -> box p) -> dia box (p -> box p)) &
	               (box dia -p -> box box dia -p) & dia box (p -> box p)
	               -> box dia p -> dia box p)],
    [tx30,20,-((box (dia q & (-p v -q)) -> box box (dia q & (-p v -q)))
	               & (box dia p -> dia box p) -> box dia p & box dia q ->
	               dia (p & q))],
    [tx31,10,-((box dia p & box dia -p -> dia (p & -p)) -> box dia p ->
	               dia box p)],
    [tx32,10,-((box dia p -> dia box p) -> box p -> dia p)],
    [tx33,10,-((box ((p v dia p) & (-p v dia -p)) -> box box ((p v dia
	               p) & (-p v dia -p))) & box (box (p & (p v dia p) & (-p
	               v dia -p)) -> box box (p & (p v dia p) & (-p v dia
	               -p))) & box (box (-p & (p v dia p) & (-p v dia -p)) ->
	               box box (-p & (p v dia p) & (-p v dia -p))) & (box dia
	               p -> dia box p) -> box (p v dia p) -> dia (p & box
	               p))],
    [tx34,10,-((box (p v dia p) -> dia (p & box p)) -> box dia p -> dia
	               box p)],
    [tx35,10,-((box (box (p & box p) -> p & box p) -> box (p & box p))
	               -> box p -> box box p)],
    [tx36,10,-((box (box false -> false) -> box false) -> box dia true
	               -> box false)],
    [tx37,10,-((box (box p -> p) -> box p) -> box (box p -> p) -> dia
	               box p -> box p)],
    [tx38,10,-((box dia true -> box false) & (box (box p -> p) -> dia
	               box p -> box p) -> box (box p -> p) -> box p)],
    [tx39,10,-((box (box (p & box (box p -> p)) -> p & box (box p ->
	               p)) -> box (p & box (box p -> p))) & box box (box (box
	               p -> p) -> box p) -> box (box (p -> box p) -> p) -> box
	               p)],
    [tx40,10,-((box (box p -> box box p) & (box (box p -> p) -> dia box
	               p -> box p) -> box (box (p -> box p) -> p) -> dia box p
	               -> box p))],
    [tx41,10,-((box (box (p -> box p) -> p) -> box box (box (p -> box
	               p) -> p)) & box (box p -> box box p) & (box (box (p ->
	               box p) -> p) -> dia box p -> p) & (box (box ((p -> box
	               p) -> box (p -> box p)) -> p -> box p) -> dia box (p ->
	               box p) -> p -> box p) -> box (box (p -> box p) -> p) ->
	               dia box p -> box p)],
    [tx42,10,-((box p -> p) & (box (box (p -> box p) -> p) -> dia box p
	               -> box p) -> box (box (p -> box p) -> p) -> dia box p
	               -> p)],
    [tx43,10,-((box (box p -> p) & (box (box (p -> box p) -> p) -> dia
	               box p -> p) -> box (box (p -> box p) -> box p) -> dia
	               box p -> p))],
    [tx44,10,-((box (box (box (p -> box p) -> box p) -> dia box p -> p)
	               -> box (box (p -> box p) -> box p) -> dia box p -> p) &
	               box (box (p -> box p) -> p -> box p) & box (box (box (p
	               -> box p) -> box p) -> dia box p -> p) -> box (box (p
	               -> box p) -> p) -> dia box p -> p)],
    [tx45,20,-((box (box p -> p) & (box (box (p -> box p) -> p) -> box
	               box (box (p -> box p) -> p)) & box (box p -> box box p)
	               & (box (box (p -> box p) -> p) -> dia box p -> p) &
	               (box (box ((p -> box p) -> box (p -> box p)) -> p ->
	               box p) -> dia box (p -> box p) -> p -> box p) -> box
	               (box (p -> box p) -> box p) -> dia box p -> box p))],
    [tx46,10,-((box p -> p) & (box (box (box (p -> box p) -> box p) ->
	               dia box p -> box p) -> box (box (p -> box p) -> box p)
	               -> dia box p -> box p) & box (box (p -> box p) -> p ->
	               box p) & box (box (box (p -> box p) -> box p) -> dia
	               box p -> box p) -> box (box (p -> box p) -> p) -> dia
	               box p -> p)],
    [tx47,10,-((box (box (p -> box p) -> p) -> dia box p -> p) -> box
	               (box (p -> box p) -> p) -> dia box p -> p v box p)],
    [tx48,10,-((box p -> p) & (box (box (p -> box p) -> p) -> dia box p
	               -> p v box p) -> box (box (p -> box p) -> p) -> dia box
	               p -> p)],
    [tx49,10,-((box (box ((box (p -> box p) -> p) & (box (box (p -> box
	               p) -> p) -> box box (box (p -> box p) -> p)) -> box
	               ((box (p -> box p) -> p) & (box (box (p -> box p) -> p)
	               -> box box (box (p -> box p) -> p)))) -> (box (p -> box
	               p) -> p) & (box (box (p -> box p) -> p) -> box box (box
	               (p -> box p) -> p))) -> (box (p -> box p) -> p) & (box
	               (box (p -> box p) -> p) -> box box (box (p -> box p) ->
	               p))) & box (box (box (p -> box p) -> p) -> p) -> box
	               (box (p -> box p) -> p) -> box p)],
    [tx50,10,-((box p -> p) & (box (box (box (p -> box p) -> p) -> box
	               p) -> box (box (p -> box p) -> p) -> box p) & box (box
	               (box (p -> box p) -> p) -> box p) -> box (box (p -> box
	               p) -> p) -> p)],
    [tx51,10,-((box (box (p -> box p) -> p) -> p) & box (box (box (p ->
	               box p) -> p) -> p) -> box (box (p -> box p) -> box p)
	               -> p)],
    [tx52,10,-((box (box (p -> box p) -> p -> box p) & (box -box (box
	               (p -> box p) -> p) -> -box (box (p -> box p) -> p)) &
	               (box (box (p -> box p) -> box p) -> p) -> box (box (p
	               -> box p) -> p) -> p))],
    [tx53,10,-((box (box ((box (p -> box p) -> box p) & (box (box (p ->
	               box p) -> p) -> p) & (box ((box (p -> box p) -> box p)
	               & (box (box (p -> box p) -> p) -> p)) -> box box ((box
	               (p -> box p) -> box p) & (box (box (p -> box p) -> p)
	               -> p))) -> box ((box (p -> box p) -> box p) & (box (box
	               (p -> box p) -> p) -> p) & (box ((box (p -> box p) ->
	               box p) & (box (box (p -> box p) -> p) -> p)) -> box box
	               ((box (p -> box p) -> box p) & (box (box (p -> box p)
	               -> p) -> p))))) -> (box (p -> box p) -> box p) & (box
	               (box (p -> box p) -> p) -> p) & (box ((box (p -> box p)
	               -> box p) & (box (box (p -> box p) -> p) -> p)) -> box
	               box ((box (p -> box p) -> box p) & (box (box (p -> box
	               p) -> p) -> p)))) -> (box (p -> box p) -> box p) & (box
	               (box (p -> box p) -> p) -> p) & (box ((box (p -> box p)
	               -> box p) & (box (box (p -> box p) -> p) -> p)) -> box
	               box ((box (p -> box p) -> box p) & (box (box (p -> box
	               p) -> p) -> p)))) & box (box (box (p -> box p) -> p) ->
	               p) -> box (box (p -> box p) -> box p) -> box p)],
    [tx54,10,-((box p -> p) & box (box (p -> box p) -> p -> box p) &
	               (box (box (p -> box p) -> box p) -> box p) -> box (box
	               (p -> box p) -> p) -> p)],
    [tx55,10,-((box (box (p -> box p) -> p) -> p) & (box (box ((box (p
	               -> box p) -> p) & (box (box (p -> box p) -> p) -> box
	               box (box (p -> box p) -> p)) -> box ((box (p -> box p)
	               -> p) & (box (box (p -> box p) -> p) -> box box (box (p
	               -> box p) -> p)))) -> (box (p -> box p) -> p) & (box
	               (box (p -> box p) -> p) -> box box (box (p -> box p) ->
	               p))) -> (box (p -> box p) -> p) & (box (box (p -> box
	               p) -> p) -> box box (box (p -> box p) -> p))) -> box
	               (box (p -> box p) -> p) -> p v box p)],
   [tx56,10,-((box p -> p) & (box (box (box (p -> box p) -> p) -> p v
	               box p) -> box (box (p -> box p) -> p) -> p v box p) &
	               box (box (box (p -> box p) -> p) -> p v box p) -> box
	               (box (p -> box p) -> p) -> p)],
   [tx57,30,-((box (box ((box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q)) -> box ((box (p -> box q) -> box q) & (box (box (p
	               -> box q) -> box q) -> box box (box (p -> box q) -> box
	               q)))) -> (box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q))) -> (box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q))) & (box (box ((box ((p -> box q) -> box (p -> box
	               q)) -> p -> box q) & (box (box ((p -> box q) -> box (p
	               -> box q)) -> p -> box q) -> box box (box ((p -> box q)
	               -> box (p -> box q)) -> p -> box q)) -> box ((box ((p
	               -> box q) -> box (p -> box q)) -> p -> box q) & (box
	               (box ((p -> box q) -> box (p -> box q)) -> p -> box q)
	               -> box box (box ((p -> box q) -> box (p -> box q)) -> p
	               -> box q)))) -> (box ((p -> box q) -> box (p -> box q))
	               -> p -> box q) & (box (box ((p -> box q) -> box (p ->
	               box q)) -> p -> box q) -> box box (box ((p -> box q) ->
	               box (p -> box q)) -> p -> box q))) -> (box ((p -> box
	               q) -> box (p -> box q)) -> p -> box q) & (box (box ((p
	               -> box q) -> box (p -> box q)) -> p -> box q) -> box
	               box (box ((p -> box q) -> box (p -> box q)) -> p -> box
	               q))) & box (box (box ((p -> box q) -> box (p -> box q))
	               -> p -> box q) -> p -> box q) -> box (box (p -> box q)
	               -> box q) & box (box (-p -> box q) -> box q) -> box
	               q)],
     [tx58,10,-((box (box (p -> box p) -> p) -> box (p -> box p) -> p) &
	               box box (box (p -> box p) -> p -> box p) & (box (box (p
	               -> box p) -> p) -> box box (box (p -> box p) -> p)) &
	               box (box p -> box box p) & (box (box (p -> box (p ->
	               box p)) -> box (p -> box p)) & box (box (-p -> box (p
	               -> box p)) -> box (p -> box p)) -> box (p -> box p)) ->
	               box (box (p -> box p) -> p) -> p)],
    [tx59,10,-((box (box (p -> box p) -> p) -> p) -> box p -> p)],
    [tx60,10,-((box (box (p & (box p -> box box p) -> box (p & (box p
	               -> box box p))) -> p & (box p -> box box p)) -> p &
	               (box p -> box box p)) -> box p -> box box p)],
    [tx61,10,-((box (box (dia -p -> box dia -p) -> dia -p) -> dia -p) &
	               (box (box (dia -p & (box dia -p -> box box dia -p) ->
	               box (dia -p & (box dia -p -> box box dia -p))) -> dia
	               -p & (box dia -p -> box box dia -p)) -> dia -p & (box
	               dia -p -> box box dia -p)) & (box (box (-box (p -> box
	               p) & (box -box (p -> box p) -> box box -box (p -> box
	               p)) -> box (-box (p -> box p) & (box -box (p -> box p)
	               -> box box -box (p -> box p)))) -> -box (p -> box p) &
	               (box -box (p -> box p) -> box box -box (p -> box p)))
	               -> -box (p -> box p) & (box -box (p -> box p) -> box
	               box -box (p -> box p))) & box (box (box (p -> box p) ->
	               p) -> p) -> box dia p -> dia box p)],
    [tx62,10,-((box (box (p -> box p) -> p) -> p) -> box (box (p -> box
	               p) -> p) -> dia box p -> p)],
    [tx63,10,-((box (box (p -> box p) -> p) -> box p) -> box (box (p ->
	               box p) -> p) -> dia box p -> box p)],
    [tx64,10,-((box (box -p -> -p) & (box dia p -> dia box p) & (box
	               (box (p -> box p) -> p) -> dia box p -> p) -> box (box
	               (p -> box p) -> p) -> p))],
    [tx65,10,-((dia box (box p -> q) -> (box p -> q) -> box (box p ->
	               q)) -> box (box p -> q) v box (box q -> p))],
    [tx66,10,-((box dia box p -> dia box p) & (dia box p -> p -> box p)
	               -> box dia box p -> p -> box p)]
	]).

